Nuprl Lemma : ecl-trans-type_wf 11,40
ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), A:ecl-trans-tuple{i:l}
ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), A:ecl-trans-tuple(ds; da). ecl-trans-type(A)  Type 
latex

Definitionst  T, ecl-trans-type(A), ecl-trans-tuple{i:l}(ds; da), Id, x. t(x), x:A. B(x), fpf(A; a.B(a)), Knd
Lemmasecl-trans-tuple wf, Knd wf, fpf wf, Id wf

origin